i:Id, l:IdLnk, da:k:Knd fp Type, tg:Id, k:Knd, n, f:Top.
msg-spec-loc-decl(k sends on l with tag tg [s,v.f(s,v)], at marker n;i;da)

source(l) = i & rcv(l,tg)  dom(da) 

latex

Definitions

t  T, P  Q, x:A. B(x), b, P & Q, <a,b>, Knd, Type, x.A(x), x. t(x), a:A fp B(a), Top, x:AB(x), rcv(l,tg), KindDeq, x  dom(f), Prop, source(l), Id, s = t, x:AB(x), IdLnk, P  Q, P  Q, type List, nil, car.cdr, (x  l), {T}, Void, x:A. B(x), IdLnkDeq, product-deq(A;B;a;b), x : v, xL. P(x), msg-spec-loc-decl(snd;i;da), k sends on l with tag tg [s,v.f(s;v)], at marker n, left+right, P  Q, Dec(P), False, A, SQType(T), s ~ t, Atom$n, 2of(t), 1of(t), True, true,

Lemmas

bool sq, assert elim, decidable assert, IdLnk sq, pi1 wf, pi2 wf, Id sq, decidable equal Id, fpf wf, fpf-single-dom, fpf-single wf, top wf, product-deq wf, idlnk-deq wf, iff functionality wrt iff, and functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, member singleton, l member wf, IdLnk wf, Id wf, lsrc wf, assert wf, fpf-dom wf, Kind-deq wf, rcv wf, fpf-trivial-subtype-top, Knd wf